V:(IdType), M1, M2:MsgA.
(x:Id. V(x)  M2.ds(x))  M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v)) 

latex

Definitions	Top, False, Unit, P  Q, , b, A, M.init(x,v), M1  M2, M.ds(x), MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), x  dom(f), IdDeq, Prop, f(x), a:A fp B(a), x. t(x), f(x)?z, x(s), IdLnk, Id, Knd, f  g, t  T, x:A. B(x), b, A & B, P  Q
Lemmas	Id wf, fpf-cap wf, fpf-trivial-subtype-top, fpf-ap wf, id-deq wf, fpf-dom wf, assert wf, ma-sub wf, ma-ds wf, msga wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, subtype rel self